package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class Toy6 {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Toy6");
		 
         // Variables
         TypedData v3 = new TypedData("v3", Constants.TYPE_INTEGER);
         tiosts.addVariable(v3);
         
         // There are no parameters       
         
         Action init2 = new Action("Init2", Constants.ACTION_INTERNAL);
         tiosts.addAction(init2);
         Action b = new Action("b", Constants.ACTION_OUTPUT);
         tiosts.addAction(b);
         tiosts.addActionParameter(v3);
         Action a = new Action("a", Constants.ACTION_OUTPUT);
         tiosts.addAction(a);         
         
         Location start = new Location("Start2");
         tiosts.addLocation(start);
         Location s4 = new Location("S4");
         tiosts.addLocation(s4);
         Location s5 = new Location("S5");
         tiosts.addLocation(s5);        
         Location s6 = new Location("S6");
         tiosts.addLocation(s6);
         
         // Initial Condition
         tiosts.setInitialCondition("v3 > 0");
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("Start2", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init2, "v3 := 0", null, "S4");
         tiosts.createTransition("S4", Constants.GUARD_TRUE, Constants.GUARD_TRUE, b, "v3 := 0", null, "S5");
         tiosts.createTransition("S4", Constants.GUARD_TRUE, Constants.GUARD_TRUE, a, "v3 := 0", null, "S6");
         
         return tiosts;		 
	 }

}
